翻訳と辞書 Words near each other ・ Skol Airlines ・ Skol Company ・ Skol Lager Individual ・ Skol Veythrin Karenza ・ Skol, Vikings ・ Skolankowska Wola ・ Skold ・ Skold vs. KMFDM ・ Skole ・ Skole Beskids ・ Skole Raion ・ Skolebrød ・ Skolelinux ・ Skolem arithmetic ・ Skolem arithmetic (disambiguation) ・ Skolem normal form ・ Skolem problem ・ Skolem's paradox ・ Skolem–Mahler–Lech theorem ・ Skolem–Noether theorem ・ Skolfield-Whittier House ・ Skolian Empire ・ Skolimowo ・ Skolin ・ Skolion ・ Skolithos ・ Skolity ・ Skolkovo ・ Skolkovo (rural locality) ・ Skolkovo Foundation Dictionary Lists mini英和辞書 mini和英辞書 Webster 1913 Latin-English FOLDOC Wikipedia English ウィキペディア

翻訳と辞書　辞書検索 [ 開発暫定版 ] スポンサード リンク Skolem normal form ： ウィキペディア英語版 Skolem normal form In mathematical logic, reduction to Skolem normal form (SNF) is a method for removing existential quantifiers from formal logic statements, often performed as the first step in an automated theorem prover. A formula of first-order logic is in Skolem normal form (named after Thoralf Skolem) if it is in prenex normal form with only universal first-order quantifiers. Every first-order formula may be converted into Skolem normal form while not changing its satisfiability via a process called Skolemization (sometimes spelled "Skolemnization"). The resulting formula is not necessarily equivalent to the original one, but is equisatisfiable with it: it is satisfiable if and only if the original one is satisfiable.〔(【引用サイトリンク】url=http://www.mpi-inf.mpg.de/departments/rg1/teaching/autrea-ss10/script/lecture10.pdf )〕 The simplest form of Skolemization is for existentially quantified variables which are not inside the scope of a universal quantifier. These may be replaced simply by creating new constants. For example, $\backslash exists\; x\; P(x)$ may be changed to $P(c)$, where $c$ is a new constant (does not occur anywhere else in the formula). More generally, Skolemization is performed by replacing every existentially quantified variable $y$ with a term $f(x\_1,\backslash ldots,x\_n)$ whose function symbol $f$ is new. The variables of this term are as follows. If the formula is in prenex normal form, $x\_1,\backslash ldots,x\_n$ are the variables that are universally quantified and whose quantifiers precede that of $y$. In general, they are the variables that are quantified universally and such that $\backslash exists\; y$ occurs in the scope of their quantifiers. The function $f$ introduced in this process is called a Skolem function (or Skolem constant if it is of zero arity) and the term is called a Skolem term. As an example, the formula $\backslash forall\; x\; \backslash exists\; y\; \backslash forall\; z.\; P(x,y,z)$ is not in Skolem normal form because it contains the existential quantifier $\backslash exists\; y$. Skolemization replaces $y$ with $f(x)$, where $f$ is a new function symbol, and removes the quantification over $y$. The resulting formula is $\backslash forall\; x\; \backslash forall\; z\; .\; P(x,f(x),z)$. The Skolem term $f(x)$ contains $x$, but not $z$, because the quantifier to be removed $\backslash exists\; y$ is in the scope of $\backslash forall\; x$, but not in that of $\backslash forall\; z$; since this formula is in prenex normal form, this is equivalent to saying that, in the list of quantifers, $x$ precedes $y$ while $z$ does not. The formula obtained by this transformation is satisfiable if and only if, the original formula is. ==How Skolemization works== Skolemization works by applying a second-order equivalence in conjunction to the definition of first-order satisfiability. The equivalence provides a way for "moving" an existential quantifier before a universal one. :$\backslash forall\; x\; \backslash Big(\; R(g(x))\; \backslash vee\; \backslash exists\; y\; R(x,y)\; \backslash Big)\; \backslash iff\; \backslash forall\; x\; \backslash Big(\; R(g(x))\; \backslash vee\; R(x,f(x))\; \backslash Big)$ where :$f(x)$ is a function that maps $x$ to $y$. Intuitively, the sentence "for every $x$ there exists a $y$ such that $R(x,y)$" is converted into the equivalent form "there exists a function $f$ mapping every $x$ into a $y$ such that, for every $x$ it holds $R(x,f(x))$". This equivalence is useful because the definition of first-order satisfiability implicitly existentially quantifies over the evaluation of function symbols. In particular, a first-order formula $\backslash Phi$ is satisfiable if there exists a model $M$ and an evaluation $\backslash mu$ of the free variables of the formula that evaluate the formula to ''true''. The model contains the evaluation of all function symbols; therefore, Skolem functions are implicitly, existentially quantified. In the example above, $\backslash forall\; x\; .\; R(x,f(x))$ is satisfiable if and only if, there exists a model $M$, which contains an evaluation for $f$, such that $\backslash forall\; x\; .\; R(x,f(x))$ is true for some evaluation of its free variables (none in this case). This may be expressed in second order as $\backslash exists\; f\; \backslash forall\; x\; .\; R(x,f(x))$. By the above equivalence, this is the same as the satisfiability of $\backslash forall\; x\; \backslash exists\; y\; .\; R(x,y)$. At the meta-level, first-order satisfiability of a formula $\backslash Phi$ may be written with a little abuse of notation as $\backslash exists\; M\; \backslash exists\; \backslash mu\; ~.~\; (\; M,\backslash mu\; \backslash models\; \backslash Phi)$, where $M$ is a model, $\backslash mu$ is an evaluation of the free variables, and $\backslash models$ means that $\backslash Phi$ is true in $M$ under $\backslash mu$. Since first-order models contain the evaluation of all function symbols, any Skolem function $\backslash Phi$ contains is implicitly, existentially quantified by $\backslash exists\; M$. As a result, after replacing an existential quantifier over variables into an existential quantifiers over functions at the front of the formula, the formula still may be treated as a first-order one by removing these existential quantifiers. This final step of treating $\backslash exists\; f\; \backslash forall\; x\; .\; R(x,f(x))$ as $\backslash forall\; x\; .\; R(x,f(x))$ may be completed because functions are implicitly existentially quantified by $\backslash exists\; M$ in the definition of first-order satisfiability. Correctness of Skolemization may be shown on the example formula $F\_1\; =\; \backslash forall\; x\_1\; \backslash dots\; \backslash forall\; x\_n\; \backslash exists\; y\; R(x\_1,\backslash dots,x\_n,y)$ as follows. This formula is satisfied by a model $M$ if and only if, for each possible value for $x\_1,\backslash dots,x\_n$ in the domain of the model there exists a value for $y$ in the domain of the model that makes $R(x\_1,\backslash dots,x\_n,y)$ true. By the axiom of choice, there exists a function $f$ such that $y\; =\; f(x\_1,\backslash dots,x\_n)$. As a result, the formula $F\_2\; =\; \backslash forall\; x\_1\; \backslash dots\; \backslash forall\; x\_n\; R(x\_1,\backslash dots,x\_n,f(x\_1,\backslash dots,x\_n))$ is satisfiable, because it has the model obtained by adding the evaluation of $f$ to $M$. This shows that $F\_1$ is satisfiable only if $F\_2$ is satisfiable as well. In the other way around, if $F\_2$ is satisfiable, then there exists a model $M\text{'}$ that satisfies it; this model includes an evaluation for the function $f$ such that, for every value of $x\_1,\backslash dots,x\_n$, the formula $R(x\_1,\backslash dots,x\_n,f(x\_1,\backslash dots,x\_n))$ holds. As a result, $F\_1$ is satisfied by the same model because one may choose, for every value of $x\_1,\backslash ldots,x\_n$, the value $y=f(x\_1,\backslash dots,x\_n)$, where $f$ is evaluated according to $M\text{'}$. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Skolem normal form」の詳細全文を読む スポンサード リンク 翻訳と辞書 : 翻訳のためのインターネットリソース Copyright(C) kotoba.ne.jp 1997-2016. All Rights Reserved.